#use "context.decls"

let tree_binsert : tree -> nat -> tree |>
  { Leaf => ( 0 => Node (Leaf, 0, Leaf)
            | 1 => Node (Leaf, 1, Leaf)
            | 2 => Node (Leaf, 2, Leaf) )
  | Node (Leaf, 1, Leaf) => ( 0 => Node (Node (Leaf, 0, Leaf), 1, Leaf)
                            | 1 => Node (Leaf, 1, Leaf)
                            | 2 => Node (Leaf, 1, Node (Leaf, 2, Leaf)) )
  | Node (Leaf, 0, Leaf) => ( 0 => Node (Leaf, 0, Leaf)
                            | 1 => Node (Leaf, 0, Node (Leaf, 1, Leaf))
                            | 2 => Node (Leaf, 0, Node (Leaf, 2, Leaf)) )
  | Node (Leaf, 2, Leaf) => ( 0 => Node (Node (Leaf, 0, Leaf), 2, Leaf)
                            | 1 => Node (Node (Leaf, 1, Leaf), 2, Leaf)
                            | 2 => Node (Leaf, 2, Leaf) )
  | Node (Node (Leaf, 0, Leaf), 1, Leaf) => ( 0 => Node (Node (Leaf, 0, Leaf), 1, Leaf)
					    | 1 => Node (Node (Leaf, 0, Leaf), 1, Leaf)
					    | 2 => Node (Node (Leaf, 0, Leaf), 1, Node(Leaf, 2, Leaf))
					    )
  | Node (Leaf, 0, Node (Leaf, 1, Leaf)) => ( 2 => Node (Leaf, 0, Node (Leaf, 1, Node(Leaf, 2, Leaf))) )
  | Node (Node (Leaf, 1, Leaf), 2, Leaf) => ( 0 => Node (Node (Node(Leaf, 0, Leaf), 1, Leaf), 2, Leaf) )
  | Node (Leaf, 1, Node (Leaf, 2, Leaf)) => ( 0 => Node (Node (Leaf, 0, Leaf), 1, Node (Leaf, 2, Leaf))
                                            | 1 => Node (Leaf, 1, Node (Leaf, 2, Leaf)) )
  | Node (Node (Leaf, 1, Leaf), 2, Leaf) => ( 0 => Node (Node (Node(Leaf, 0, Leaf), 1, Leaf), 2, Leaf) )
  } = ?
